$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$), $n$:$\mathbb{N}$.
\\[0ex](ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $A$)($n$,[])) $\Leftarrow\!\Rightarrow$ False